(in-package "ACL2")
(include-book "../../include/src/io-utilities")
(include-book "../../include/src/binary-io-utilities")
(include-book "grid")
(set-state-ok t)


;;==================UTILITIES=============================


;; Helper function that converts
;; a list of values to their actual value
;; given the transformation base (b).
;; @param b The base value.
;; @param xs The list of values.
;; @return A natural number represented by the list xs.
(defun numeral->nat* (b xs)
    (if (consp xs)
        (+ (car xs) (* b (numeral->nat* b (cdr xs))))
        0))


;; Converts a list of bytes to their corresponding
;; natural number representation.
;; @param xs The list of bytes.
;; @return A natural number represented by xs.
(defun bytes->nat* (xs)
  (numeral->nat* 256 xs))


;; Converts a natural number into the corresponding
;; list of bytes.
;; @param n The number to be transformed
;; @return A list of bytes (Numbers < 256)
(defun nat->bytes* (n)
    (if (zp n)
        nil
        (cons (mod n 256)
              (nat->bytes* (floor n 256)))))


;; Gets the first n elements of list l
;; @param n The number of elements.
;; @param l The list.
;; @return A list counting the first n elements of l.
(defun firstn (n l)
  (cond ((endp l) nil)
        ((zp n) nil)
        (t (cons (car l)
                 (firstn (1- n) (cdr l))))))


;; Helper function that appends extra "empty" bytes
;; to the end of a byte list until the list is of
;; length (num).
;; @param bytes The list of bytes.
;; @param num Tne number of bytes the list needs to be in
;;            in length.
;; @return A byte list with (num) trailing "empty" bytes.
(defun add-zeroes* (bytes num)
  (if (< (len bytes) num)
      (add-zeroes* (reverse (cons 0 (reverse bytes))) num) 
      bytes))


;; Given a specific number (val) this will create
;; a list of bytes of length (num).
;; @param val The number that is being converted.
;; @param num The length the byte list needs to be.
;; @param A byte list of size (num) representing (val).
(defun get-bytes* (val num)
  (let* ((bytes (nat->bytes* val)))
    (if (< (len bytes) num)
        (add-zeroes* bytes num)
        bytes)))




;;==================PALETTE/HEADER=============================


;; Using a Windows BMP 54 Byte Header with 8 bit pixels
(defconst *header-size* 54)
(defconst *bpp* 8)


;; Calculates the size of a row with the necessary padding.
;; @param width The width of the image
;; @return The size of the row with padding.
(defun calculate-rowsize* (width)
  (* (floor (+ (* *bpp* width) 31) 32) 4))


; Creates a color element for the
; palette. Given the method this will
; create a color that is on the grey scale.
; @param idx The index of the color.
; @return The list of bytes that represent a single color.
(defun create-color* (idx)
  (list idx idx idx 0))
 

; Creates a list or bytes that represents
; the color table for this bitmap. It will
; generate 255 colors working recursively.
; @param palette The working byte list.
; @param idx The index in the 255 colors that we are on
; @return The list of bytes acting a palette.
(defun create-palette* (palette idx)
  (if (< idx 256)
      (create-palette* (append palette (create-color* idx)) (+ idx 1))
      palette))


; Checks to see if the pixel is set to black.
; It does this by evaluating if the pixel's
; byte representation can be evaluated to 0.
; In the common color palette this is black
; and in our grey scale palette it is also black.
; @param pixel The byte representation of the pixel.
; @return True if the pixel is 0, false otherwise.
(defun is-alive* (pixel)
  (if (= (bytes->nat* pixel) 255)
      t
      nil))


;; Given a width and height this function
;; will create the header for a bitmap file
;; with properties reflected by that height
;; and width.
;; @param width The width in pixels of the image.
;; @param height The height in pixels of the image.
;; @return The header of a bitmap given as an array
;;         of bytes.
;;
(defun create-bitmap-head* (rowsize width height)
  (let* ((size (* rowsize height)))
  (append 
   ;The bitmap signature
   (list (char-code #\B) (char-code #\M))
   ;The estimated size, this is not accurate
   (get-bytes* (+ *header-size* size) 4)
   ;Reserved space
   (list 0 0 0 0)
   ;Offset to image data in bytes
   (list *header-size* 4 0 0)
   ;The bitmap info header
   (list 40 0 0 0)
   ;Set the width and the height
   (get-bytes* width 4)
   (get-bytes* height 4)
   ;Set the number of planes
   (list 1 0)
   ;Set the bits per pixel. -- 24
   (list *bpp* 0)
   ;Compression type -- None
   (list 0 0 0 0)
   ;The size of the image data. --> Not the header
   (get-bytes* size 4)
   ;Horizontal resolution -- Default
   (list 0 0 0 0)
   ;Vertical Resolution -- Default
   (list 0 0 0 0)
   ;Number of colors irrelevant for 24-bit
   (list 0 0 0 0)
   ;Number of important colors irrelevant for 24-bit
   (list 0 0 0 0)
   (create-palette* nil 0)
   )))

(defconst *alive* 255)
(defconst *dead* 0)

;;==================SAVING=============================


; This function will return the byte representing black
; or the byte representing white in the grey scale
; pallette 
; @param cell True if cell is alive, false otherwise.
; @return The white or the black color byte in grey scale
;         palette.
(defun convert-cell-to-pixel* (cell)
  (if cell
      *alive*
      *dead*))


;; This will convert a single row of cells into an
;; array of pixels. This will apply any necessary
;; padding to the row.
;; @param type The type of grid. Used to get the cells 
;;             acording to grid type.
;; @param grid The grid with all of the cells.
;; @param h-idx The current heighth index that this row is on.
;; @param left The left element. Used as iterator.
;; @param right The right most element.
;; @param rowsize The necessary size of row with padding.
;; @param row Tail recursive list element returned at end.
;; @returns The row of pixels for each cell in row.
(defun convert-row* (type_ grid h-idx left right rowsize row)
  (if (< left (+ right 1)) ;Include the right most
      (convert-row* type_ 
                    grid 
                    h-idx 
                    (+ 1 left) 
                    right
                    rowsize
                    (reverse (cons (convert-cell-to-pixel* 
                                    (type-get type_ grid left h-idx))
                                   (reverse row)))) ;Add to end
      ;Apply padding to the row if necessary.
      (add-zeroes* row rowsize)))
                                                     

;; Iterates through each row creating a new list of byte
;; elements that represents the cells in that row.
;; @param type The type of grid. Used to get the cells 
;;             acording to grid type.
;; @param grid The grid with all of the cells.
;; @param bottom The bottom most element. Used as an iterator.
;; @param top The top most element.
;; @param left The left most element.
;; @param right The right most element.
;; @param rowsize The necessary size of row with padding.
;; @param pixels Tail recursive list element returned at end.
;; @returns The total array of pixels converted from the grid's cells.
(defun convert-rows* (type_ grid bottom top left right rowsize pixels)
  (if (< bottom (+ top 1)) ;Include the top most
      (convert-rows* type_
                     grid
                     (+ 1 bottom)
                     top
                     left
                     right
                     rowsize
                     (append pixels
                             (convert-row* type_ grid bottom left 
                                           right rowsize nil)))
      pixels))


;; Sets up the conversion for life-like grids to a pixel array.
;; @param grid The cells.
;; @param bounds The extreme points where cells reside.
;; @param rowsize The size a row must be with padding.
(defun convert-life-cells-to-pixels* (grid bounds rowsize)
  (convert-rows* t
                 grid
                 (ll-bounds-bottom bounds)
                 (ll-bounds-top bounds)
                 (ll-bounds-left bounds)
                 (ll-bounds-right bounds)
                 rowsize
                 nil))


;; Sets up the conversion for elementary grids to a pixel array.
;; @param grid The cells.
;; @param bounds The extreme points where cells reside.
;; @param rowsize The size a row must be with padding.
(defun convert-elem-cells-to-pixels* (grid bounds rowsize)
  (convert-rows* nil 
                 grid
                 0
                 0
                 (el-bounds-left bounds)
                 (el-bounds-right bounds)
                 rowsize
                 nil))


;; Generates the image from the grid that is a 
;; life like implementation.
;; @param grid The grid image.
;; @return The byte list representing the image.
(defun generate-life-image* (grid)
  (let* ((bounds (get-ll-bounds grid))
         (width (+ 1 (- (ll-bounds-right bounds) 
                   (ll-bounds-left bounds))))
         (height (+ 1 (- (ll-bounds-top bounds)
                    (ll-bounds-bottom bounds))))
         (rowsize (calculate-rowsize* width)))
    (append (create-bitmap-head* rowsize width height) 
            (convert-life-cells-to-pixels* grid bounds rowsize))))


;; Generates the image from the grid that is a 
;; elementary implemention.
;; @param grid The grid image.
;; @return The byte list representing the image.
(defun generate-elem-image* (grid)
  (let* ((bounds (get-el-bounds grid))
         (width (+ 1 (- (el-bounds-right bounds)
                   (el-bounds-left bounds))))
         (height 1)
         (rowsize (calculate-rowsize* width)))
    (append (create-bitmap-head* rowsize width height) 
            (convert-elem-cells-to-pixels* grid bounds rowsize))))


;; Given a grid this will construct an array
;; of bytes representing a bitmap image.
;; @param grid The grid object that we are attempting
;;             to represent as an image.
;; @param type The type of the grid that we are loading
;;             in the future this will be a check for
;;             additional types instead just existence.             
;; @return An array of bytes representing the grid.
(defun image-generator* (grid type_)
  (if type_
      (generate-life-image* grid)
      (generate-elem-image* grid)))


;;==================LOADING=============================


; Takes a pixel in byte representation and
; returns whether the pixel is either alive or
; dead by evaluating the color of the pixel.
; @param pixel The byte representation of pixel.
; @return True if the pixel is "alive", false otherwise.
(defun convert-pixel-to-cell* (pixel)
  (if (= *alive* (bytes->nat* pixel)) ;alive
      t
      nil))

;; Converts a single row of pixels into their cell
;; representations and inserts them into a grid.
(defun convert-pixelrow* (type_ pixels grid width bypp w-idx h-idx)
  (if (< w-idx width)
      (convert-pixelrow* type_
                         (nthcdr bypp pixels)
                         ;(cons (convert-pixel-to-cell* 
                         ;          (firstn bypp pixels)) grid)
                         (set-type type_ grid w-idx h-idx 
                                   (convert-pixel-to-cell* 
                                    (firstn bypp pixels)))
                         width
                         bypp
                         (+ 1 w-idx)
                         h-idx)
      grid))
                                   

;; Converts all of the rows by skipping forward by
;; the row size after a row is complete. The single
;; rows are processed by the convert pixel row function.
(defun convert-pixelrows* (type_ pixels width height 
                                rowsize bypp h-idx grid)
  (if (< h-idx height)
      (convert-pixelrows* type_
                          (nthcdr rowsize pixels)
                          width height rowsize
                          bypp (+ h-idx 1)
                          (convert-pixelrow* type_
                                             pixels
                                             grid
                                             width
                                             bypp
                                             0
                                             h-idx))
      grid))

;; Converts the array of pixels to a grid. The type
;; is inferred from the height of the image.
;; a height of 1 is assumed to be elementary.
;; @param pixels The array of pixel data.
;; @param width The width of the image.
;; @param height The height of the image.
;; @param bpp The bits per pixel
;; @return A grid.
(defun convert-pixels-to-cells* (pixels width height bpp)
  (let* ((type_ (> height 1))
         (grid (empty-tree)))
    (convert-pixelrows* type_ pixels width 
                        height (calculate-rowsize* width) 
                        (/ bpp 8) 0 grid))) ;Get the bytes per pixel
    


;; Reads the header and creates a list consisting
;; of the offset to pixels, the width, the height,
;; and finally the bits per pixel in that order.
;; @param image The byte array for the image.
;; @return The list of important information from header.
(defun read-bitmap-header* (image)
  (let* ((offset (bytes->nat* (firstn 4 (nthcdr 10 image))))
         (width (bytes->nat* (firstn 4 (nthcdr 18 image))))
         (height (bytes->nat* (firstn 4 (nthcdr 22 image))))
         (bpp (bytes->nat* (firstn 2 (nthcdr 28 image)))))
    (list offset width height bpp)))


;; Reads the image byte array and constructs the
;; appropriate grid type based on header information.
;; @param image The byte array for the image.
;; @return The appropriate populated grid.
(defun read-image-to-grid* (image)
  (let* ((head (read-bitmap-header* image)))
    (convert-pixels-to-cells* (nthcdr (car head) image)
                              (cadr head)
                              (caddr head)
                              (cadddr head))))


;;==================PUBLIC=============================


;; Creates a image byte array from a given
;; grid and attempts to write that data to the given
;; file location.
;; @param grid The grid object
;; @param path The location that we are writing to.
;; @return The state with any errors if there was
;;         a failure.
(defun image-save (grid type_ path state)
  (let* ((img-data (image-generator* grid type_)))
    (mv-let (error-close state)
            (byte-list->binary-file path img-data state)
            (if error-close
                (mv error-close state)
                (mv "Success" state)))))
  
;; Gets the string representing the bitmap image
;; from the given image path.
;; @param path The string representing the path
;;             the file location of the image.
;; @return A new grid object based on the bitmap image.
(defun image-load (path state)
  (mv-let (image error-open state)
          (binary-file->byte-list path state)
          (if error-open
              (mv error-open state)
              (mv (read-image-to-grid* image) state))))

(defconst *test* (set-type t (set-type t
                                       (empty-tree)
                                       0 3 t) 0 0 t))


;(generate-life-image* *test* )

;(type-get t (car (image-load "y.bmp" state)) 0 4)
; Test functions.
;(byte-list->binary-file "y.bmp" (append (create-bitmap-head* 8 5 4) *test*) state)